The article investigates a system of polymorphically typed combinatory logic which is equivalent to Gödel’s T. A notion of (strong) reduction is defined over terms of this system and it is proved that the class of well-formed terms is closed under both bracket abstraction and reduction. The main new result is that the number of contractions needed to reduce a term to normal form is computed by an ε 0-recursive function. The ordinal assignments used to obtain this result are also (...) used to prove that the system under consideration is indeed equivalent to Gödel’s T. It is hoped that the methods used here can be extended so as to obtain similar results for stronger systems of polymorphically typed combinatory terms. An interesting corollary of such results is that they yield ordinally informative proofs of normalizability for sub-systems of second-order intuitionist logic, in natural deduction style. (shrink)

This article investigates a theory of type assignment (assigning types to lambda terms) called ETA which is intermediate in strength between the simple theory of type assignment and strong polymorphic theories like Girard’s F (Proofs and types. Cambridge University Press, Cambridge, 1989). It is like the simple theory and unlike F in that the typability and type-checking problems are solvable with respect to ETA. This is proved in the article along with three other main results: (1) all primitive recursive functionals (...) of finite type are representable in ETA; (2) every term typable in ETA has a unique normal form; (3) there is a function defined by ${{\varepsilon}_0}$ -recursion which takes every typable term to a natural number which is an upper bound to the lengths of all βη-reduction sequences starting with that term. (shrink)

By "proper name" I mean a proper name in Frege's sense, i.e., a singular term. The "problem" mentioned in the title is whether the subject-term of an existential statement can be a proper name. I concentrate on examining some of the existing attempts to define "proper name" and conclude that, whatever answer is given to the question just posed, the authors of these attempts (Dummett, C Wright and B Hale) will have to modify some of their beliefs. My own favored (...) solution is to say that it can, sometimes denoting a non-existent object. (shrink)

Sections 1 through 4 define, in the usual inductive style, various classes of object including one which is called the “combinatory terms of polymorphic type”. Section 5 defines a reduction relation on these terms. Section 6 shows that the weak normalizability of the combinatory terms of polymorphic type entails the weak normalizability of the lambda terms of polymorphic type. The entailment is not vacuous, because the combinatory terms of polymorphic type are indeed weakly normalizable, as is proven in Sect. 7 (...) using Tait and Girard’s computability predicates. The remainder of the paper is devoted to arguing that interesting consequences would follow from the existence of an “ordinally informative” proof, i.e. one which uses transfinite induction over recursive ordinal numbers and otherwise finitary methods, of normalizability for as large a class of the terms as possible. (shrink)

William R. Stirton; III*—The Logical Status of ‘Exists’, Proceedings of the Aristotelian Society, Volume 95, Issue 1, 1 June 1995, Pages 37–50, https://doi.org/.

Proof-theoretic semantics is an approach to logical semantics based on two ideas, of which the first is that the meaning of a logical connective can be explained by stipulating that some mode of inference, e.g., a natural deduction introduction or elimination rule, is permissible. The second idea is that the soundness of rules which are not stipulated outright may be deduced by some proof-theoretic argument from properties of the rules which are stipulated outright. I examine the first idea. My main (...) conclusion is that the idea is more problematic, and requires more discussion, than has been generally realized. I mention five problems which will have to be overcome before the idea can be accepted as definitely viable. (shrink)

William R. Stirton; III*—The Logical Status of ‘Exists’, Proceedings of the Aristotelian Society, Volume 95, Issue 1, 1 June 1995, Pages 37–50, https://doi.org/.